Various methods are known in the art for automatically solving propositional satisfiability (SAT) problems. Most modern SAT-checkers are variations on the well-known Davis-Putnam procedure, which performs a backtracking search through a decision tree. At each node in the tree, the procedure chooses and tests an assignment, i.e., it selects a variable and assigns a Boolean value to the variable. The well-known unit clause rule is then used iteratively to deduce the assignments of additional variables, based on the assignment under test, in a procedure known as Boolean Constraint Propagation (BCP). If a given assignment is tested and is found to lead to a contradiction, the tree is pruned, using logical rules to remove paths that will not yield fruitful results.
For efficient BCP processing, it is useful to frame the SAT problem in conjunctive normal form (CNF). A CNF formula φ on n binary variables x1, . . . , xn is a conjunction (AND) of m “clauses” ω1, . . . , ωm each of which is a disjunction (OR) of one or more “literals.” A literal is an occurrence of one of the variables or its complement (NOT). It is known in the art that any Boolean expression can be cast in CNF, and there are automatic tools available for transforming arbitrary Boolean expressions to CNF. The SAT problem is solved when an assignment to the variables x1, . . . , xn is found that makes all the clauses true, or when it is proved that there is no such assignment.
“GRASP” (Generic seaRch Algorithm for the Satisfiability Problem) is an efficient tool for solving SAT problems, using the CNF representation. GRASP is described by Marques-Silva and Sakallah in “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers 48:5 (May, 1999), pages 506–516, which is incorporated herein by reference. A simplified pseudocode listing, giving a general framework for solving SAT problems, which is used in most modern SAT solvers (including GRASP) is presented below in Table I:
TABLE IBACKTRACK SEARCH ALGORITHM//Input arg: Current decision level d//Return value://SAT( ) :{SATISFIABLE, UNSATISFIABLE}//Decide( ):{DECISION, ALL-DECIDED}//Deduce( ) :{OK, CONFLICT}//Diagnose( ):{SWAP, BACK-TRACK}SAT (d){11:if (Decide (d) == ALL-DECIDED) return SATISFIABLE;12:while (TRUE) {13:if (Deduce(d) != CONFLICT) {14:if (SAT (d+1) == SATISFIABLE) returnSATISFIABLE;15 :else if (β < d || d == 0) // β iscalculated in Diagnose ( )16:{ Erase (d); return UNSATISFIABLE; }}17:if (Diagnose (d) == BACK-TRACK) returnUNSATISFIABLE;}}
At each decision level d in the search tree, a variable assignment Vd={T,F} is selected using the Decide( ) function. If all of the variables are already decided (as indicated by ALL-DECIDED), it implies that a satisfying assignment has been found, and SAT returns SATISFIABLE. This outcome indicates, in the case of BMC, that a counterexample exists. Otherwise, Deduce( ) is used to find the implied assignments and to determine whether a conflict exists, i.e., whether given the actual assignments that have been made so far, it is possible to assign the remaining variables in such a way that the SAT formula will be true. A conflict typically arises if a given unassigned variable must be simultaneously TRUE to satisfy one of the clauses and FALSE to satisfy another. If there is no conflict, the SAT procedure is called recursively at the next decision level. Otherwise, Diagnose( ) is called to analyze the conflict and decide on the next step.
Diagnose( ) identifies the assignments that led to the conflict and determines whether Vd is one of them. If so, the value of Vd is swapped, and Deduce( ) is repeated. If the swapped assignment also fails, it means that Vd is not responsible for the conflict. In this case, Diagnose( ) indicates that the procedure should BACK-TRACK to a lower decision level β. The procedure will then backtrack d-β levels, each time using Erase( ) to remove the current decision and its implied assignments before continuing the search. Marques-Silva and Sakallah present a method for computing β in the above-mentioned article.
The analysis of conflicts found by the above method allows “conflict clauses” to be computed and added to the CNF formula (also referred to as the “clause database”) as constraints on the search. A conflict clause represents an auxiliary sub-formula, such that any assignment that fails to satisfy the sub-formula will invariably lead to a conflict in the original formula. For example, suppose that during BCP it is found that the assignment of variables x=T, y=F and z=F inevitably leads to a conflict, i.e., the conjunction of these assignments represents a sufficient condition for the conflict to arise. Consequently, the negation of this conjunction must be satisfied if the instance is satisfiable. We can therefore add the new conflict clause, π=(xyz), to the clause database, with the hope that it will speed up the search. The conjunction of π with φ will cause the search procedure to backtrack immediately if the conflicting assignment is repeated. Adding conflict clauses thus constrains the search space for subsequent iterations, making the SAT problem easier to solve and reducing computation time.
Incremental Satisfiability and Pervasive Conflict Clauses
In many types of SAT problems, multiple, related SAT instances must be solved. In such cases, it is useful to reuse information (the conflict clauses) found in one instance in order to solve the next instance more efficiently. Hooker first suggested a method for incremental solution of SAT problems in “Solving the Incremental Satisfiability Problem,” Journal of Logic Programming 15 (1993), pages 359–363, which is incorporated herein by reference. He proposed an algorithm that accepts a satisfiable instance and an additional clause, and checks whether satisfiability is preserved when the new clause is added to the formula. His experiments showed that solving large instances incrementally can be faster than solving them as one monolithic formula.
This idea was extended by Kim et al. in “Incremental Boolean Satisfiability and its Application to Delay Fault Testing,” IEEE/ACM International Workshop on Logic Synthesis—IWLS'99 (June, 1999), which is also incorporated herein by reference. The authors used the technique for path delay fault testing, a process in which the effect of faults on delays in certain paths is checked. The large number of paths in such systems typically requires the partition of the problem into a series of instances, each representing a subset of the tested paths. All the paths share the same prefix P, which empirically is far larger than the suffixes s1 . . . si. Incremental satisfiability is then used in the following way: A satisfying assignment for P is sought, and conflict clauses are added to P (those clauses that are deducible directly from P). If P is unsatisfiable, the process halts because the conjunction of P with Si for all i is obviously unsatisfiable. Otherwise, the trace is used as an initial assignment when checking each of the instances PSi for all i. In case the initial trace does not lead to a satisfying assignment, the standard backtrack process is invoked.
A further extension to this idea was proposed for use in Automatic Test Pattern Generation (ATPG) by Marques-Silva and Sakallah, in “Robust Search Algorithms for Test Pattern Generation,” Proceedings of the IEEE Fault-Tolerant Computing Symposium (June, 1997), which is incorporated herein by reference. The authors apply their GRASP SAT solving tool to generate test patterns, for use in finding faults in electronic circuit designs. Some of the conflict clauses that are computed during SAT solving of these instances are independent of the given target fault model and depend only on the function and structure of the circuit under test. These conflict clauses are declared “pervasive” conflict clauses, and they can be shared among different SAT instances that are used to generate test patterns for different target fault states in the same circuit. The authors note, however, that the question of how to identify pervasive conflict clauses outside the fixed framework of the circuit formula itself remains an open issue.